$\forall$$T$:Type, $L$:$T$ List, $R$:(\{$x$:$T$$\mid$ ($x$ $\in$ $L$) \}$\rightarrow$Realizer).
\\[0ex]($\forall$$x$$\in$$L$. R{-}Feasible($R$($x$)))
\\[0ex]$\Rightarrow$ ($\forall$$x$$\in$$L$. $\forall$$y$$\in$$L$. $R$($x$) $\parallel$ $R$($y$) $\vee$ $x$ $=$ $y$ $\in$ $T$)
\\[0ex]$\Rightarrow$ R{-}Feasible($\oplus$$x$$\in$$L$.$R$($x$))